COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Stanford Verification Group Report No. 11
C00005 ENDMK
C⊗;
Stanford Verification Group Report No. 11

Stanford PASCAL Verifier User Manual

D.C. Luckham, S.M. German, F.W. v.Henke, R.A. Karp, P.W. Milne,
D.C. Oppen, W. Polak and W.L. Scherlis

The Stanford Pascal verifier is an interactive program verification system.
It automates much of the work necessary to analyze a program for consistency
with its documentation, and to give a rigorous mathematical proof of such
consistency or to pin-point areas of inconsistency.  It has been shown to have
applications an an aid to programming, and to have potential for development
as a new and useful tool in the production of reliable software.

This verifier is a prototype system.  It has inadequacies and shortcomings.
It is undergoing continuous improvement, and is expected to be used
eventually in conjunction with other kinds of program analyzers.  The
purpose of this manual is to introduce the verifier to a wider group of
users for experimentation.  We hope to encourage both feedback to help
improve this system, and the development of other program analyzers.

The verfier is coded in Maclisp, a version of Lisp developed at M.I.T.
for PDP-10 computers.  Versions of the verifier run under the TOPS 20
operating system and the Stanford WAITS operating system.